M1, M2:MsgA. M1  M2  (a:Id, s:M2.state. M2.pre(a,s)  M1.pre(a,s)) 

latex

Definitions	x:AB(x), P  Q, x:A  B(x), A c B, b, x:A. B(x), t  T, f  g, Id, Knd, IdLnk, , Type, State(ds), x.A(x), x. t(x), a:A fp B(a), Top, f(x), f(a), IdDeq, x  dom(f), , z != f(x)  P(a;z), P & Q, Valtype(da;k), MsgA, M1  M2, M.state, M.pre(a,s)
Lemmas	msga wf, ma-sub wf, ma-st wf, fpf-dom wf, Id wf, id-deq wf, assert wf, fpf-ap wf, fpf-trivial-subtype-top, ma-state wf, bool wf